First order predicate calculus is a form of logic which includes fixed values such as 'Socrates', or '42', variables that stand for unknown values and predicates, such as 'is_mortal', but makes a strong sepaaration between predicates and variables. This allows reasoning about the values and variables using the predicates, including the classic {[sylogism}}:
is_human(x)=>is_mortal(x) AND is_human(Socrates)=>is_mortal(x) IMPLIES is_mortal(Socrates)
This separation makes it relatively easy to automate reasoning, but means it is not possible to perform higher level statements or reasoning about the predicates themselves such as "is_equal is transitive".
Used on Chap. 2: page 20